COMP3141 Software System Design and Implementation

COMP3141: Software System Design and Implementation

Term 2, 2022

Quiz (Week 9)

Table of Contents

1 Phantom Types

1.1 Recognizing phantom types

1.1.1 Question 1

Consider the following type definitions. 

data Day we
  = Mon | Tue | Wed | Thu | Fri
  | Sat we | Sun we

data Free
data Taken
data Locker state = Locker (Maybe Int)

data List1 a b = List1 [b]
data List2 a b = Nil | List2 b (List2 a b)

Which of the types above are phantom types?

  1. ✗Day
  2. ✗Free
  3. ✔Locker
  4. ✔List1
  5. ✗List2

A phantom type is a data type that has some type parameter which does not occur in the type of any argument to any of its constructors.

Day has only one type parameter we, which does occur as an argument to two constructors, Sat and Sun. Consequently, Day is not a phantom type.

Free has no type parameters, and is therefore not a phantom type.

Locker has one type parameter state, and this type parameter does not occur in the type of any constructor argument. Therefore, this is a phantom type.

List1 has two type parameters, a and b. Out of these, the first one does not occur in the type of any constructor argument, which makes List1 a phantom type.

The constructor arguments of List2 both occur in the type of some constructor argument, so List2 is not a phantom type under the definition used in this course. Note, however, that List1 and List2 are essentially the same type, even though one is phantom and the other is not. This is the borderline case mentioned in the lecture.

1.2 Safe Division

We used phantom types to avoid divide-by-zero errors as follows: 

data Zero
data NonZero
data CheckedInt t = Checked Int

safeDiv :: Int -> CheckedInt NonZero -> Int
safeDiv x (Checked y) = x `div` y

1.2.1 Question 2

Which of the following statements are true?

  1. ✔The type argument t does not occur in the type of Checked.
  2. ✗The types Zero and NonZero are both phantom types.
  3. ✗This code will not compile as Zero and NonZero have not been defined.
  4. ✗The pattern matching in safeDiv is non-exhaustive (i.e. missing cases).

Zero and NonZero are types that do not have any constructors, but not phantom types. Such empty types are accepted by modern Haskell compilers.

The safeDiv function is fully defined: there is one constructor Checked, and it's accounted for.

1.2.2 Question 3

Which of the following could be a valid type signature for a function add that calculates the sum of two CheckedInt values?

  1. ✗CheckedInt NonZero -> CheckedInt NonZero -> CheckedInt NonZero
  2. ✗CheckedInt a -> CheckedInt a -> CheckedInt a
  3. ✔CheckedInt a -> CheckedInt b -> Int
  4. ✗CheckedInt a -> CheckedInt b -> CheckedInt c

The sum of two CheckedInt NonZero values can be zero: consider e.g. Checked 2 and Checked (-2). This rules out Option 1 and Option 2.

Option 4 is ruled out as well, as it could be used to get add (Checked 2) (Checked (-2)) :: CheckedInt NonZero.

1.2.3 Question 4

Choose the best type to give to a smart constructor for the type CheckedInt!

  1. ✗check :: Int -> CheckedInt NonZero
  2. ✗check :: Int -> CheckedInt (Either Zero NonZero)
  3. ✗check :: Int -> CheckedInt t
  4. ✔check :: Int -> Either (CheckedInt Zero) (CheckedInt NonZero)

A smart constructor is a function that checks or ensures a condition in order to establish an invariant for a particular type.

As it's meant to replace a regular data constructor, we expect it to be total, and so the type of Option 1 is incorrect, as check 0 would be undefined.

Option 2 is also incorrect, as Either Zero NonZero isn't one of the intended tags for our phantom type.

Option 3 is also incorrect, as this returns a CheckedInt t for any t, so it may for example apply the NonZero type tag to zero values.

The correct answer is option 4, which can return a CheckedInt Zero if the input is 0 and a CheckedInt NonZero otherwise.

1.3 Data Kinds

Here we use phantom types with an argument of kind Size to make vectors of various dimensions. Note that the vector size is not statically checked by the default V data constructor. We must be sure to only use the given smart constructors that establish the length invariant about the data: 

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}

data Size = OneD  | TwoD | ThreeD
newtype Vector (s :: Size) a = V [a]

vec1D :: a -> Vector OneD a
vec1D a = V [a]

vec2D :: (a, a) -> Vector TwoD a
vec2D (a,b) = V [a,b]

vec3D :: (a, a, a) -> Vector ThreeD a
vec3D (a,b,c) = V [a,b,c]

1.3.1 Question 5

Which of the following implementations of vector addition ensure via a static check that the precondition that the vectors must be the same size (and only that precondition), as well as the postcondition that the output vector will be the same size as the input?

  1. ✗
    addV :: (Num n) => Vector a n -> Vector b n -> Vector c n
addV (V xs) (V ys) = V (zipWith (+) xs ys)
  2. ✔
    addV :: (Num n) => Vector a n -> Vector a n -> Vector a n
addV (V xs) (V ys) = V (zipWith (+) xs ys)
  3. ✗
    addV :: (Num n) => Vector TwoD n -> Vector TwoD n -> Vector TwoD n
addV (V xs) (V ys) = V (zipWith (+) xs ys)
  4. ✗
    addV :: (Num n) => Vector a n -> Vector a n -> Vector b n
addV (V xs) (V ys) = V (zipWith (+) xs ys)

Option 1 allows the input vectors to be any size, and produces an output vector with an arbitrary size tag, which may not accurately reflect the size of the contents, so it is incorrect. Option 3 requires that both input vectors are two-dimensional and the output vector is also two-dimensional. This is too excessive a restriction, as we only require that the sizes are equal. Option 4 allows the output vector to have an arbitrary size tag, which is also incorrect.

Option 2 requires both input vectors to have the same size a and then returns a vector of the same size. This is the correct answer.

1.3.2 Question 6

Suppose we made a Matrix type using vectors of vectors: 

type Matrix r c a = Vector r (Vector c a)

What would be a correct type for a matrix multiplication function?

  1. ✗mm :: Num a => Matrix r i a -> Matrix r i a -> Matrix r i a
  2. ✗mm :: Num a => Matrix r i a -> Matrix i c a -> Matrix r i a
  3. ✗mm :: Num a => Matrix r i a -> Matrix c i a -> Matrix i i a
  4. ✔mm :: Num a => Matrix r i a -> Matrix i c a -> Matrix r c a

Matrix multiplication of \(A \times B\) requires the number of columns in \(A\) be the same as the number of rows in \(B\). The result will have the same number of rows as \(A\) and the same number of columns as \(B\). Thus, option 4 is correct.

Option 1 requires the matrices have the same exact dimensions. Option 2 makes the output the same size as \(A\). Option 3 incorrectly mixes the dimensionalities of the inputs.

1.4 Static Assurance

1.4.1 Question 7

Select all true statements below.

  1. ✗Testing is the most common form of static analysis.
  2. ✗You can compile and run your Haskell program even if it fails type checking.
  3. ✔Types and model checkers are forms of static assurance.
  4. ✔Static means of assurance can analyze programs without running them.

Testing is not a form of static analysis, as it requires executing the program that's being tested. As you've experienced in this course, you cannot compile a Haskell program if it fails type checking. The other options are correct.

1.4.2 Question 8

Which of the following is ruled out by Rice's theorem?

  1. ✗Deciding whether a program contains a while loop.
  2. ✔Deciding whether a computable function always returns non-zero output.
  3. ✗Deciding whether a Haskell program has type Int -> Int.
  4. ✗Deciding whether a Haskell program has type Int -> CheckedInt NonZero.

Rice's theorem rules out the existence of a program that checks if any given computable function from the natural numbers to the natural numbers ever returns zero: this is a non-trivial property of partial computable functions.

Nonetheless, Haskell type-checking is decidable, even in the case of Option 4.

Submission is already closed for this quiz. You can click here to check your submission (if any).

2022-09-06 Tue 00:54

Announcements RSS